<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>
<title>Stmt</title>
<link rel="stylesheet" type="text/css" href="../../stylesheet.css" title="Style">
</head>
<body>
<script type="text/javascript"><!--
    if (location.href.indexOf('is-external=true') == -1) {
        parent.document.title="Stmt";
    }
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar_top">
<!--   -->
</a><a href="#skip-navbar_top" title="Skip navigation links"></a><a name="navbar_top_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/lang/SeqAssigner.html" title="class in mmj.lang"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/lang/Sym.html" title="class in mmj.lang"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/lang/Stmt.html" target="_top">Frames</a></li>
<li><a href="Stmt.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li><a href="#field_summary">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li><a href="#field_detail">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">mmj.lang</div>
<h2 title="Class Stmt" class="title">Class Stmt</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li>java.lang.Object</li>
<li>
<ul class="inheritance">
<li><a href="../../mmj/lang/MObj.html" title="class in mmj.lang">mmj.lang.MObj</a></li>
<li>
<ul class="inheritance">
<li>mmj.lang.Stmt</li>
</ul>
</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<dl>
<dt>Direct Known Subclasses:</dt>
<dd><a href="../../mmj/lang/Assrt.html" title="class in mmj.lang">Assrt</a>, <a href="../../mmj/lang/Hyp.html" title="class in mmj.lang">Hyp</a></dd>
</dl>
<hr>
<br>
<pre>public abstract class <span class="strong">Stmt</span>
extends <a href="../../mmj/lang/MObj.html" title="class in mmj.lang">MObj</a></pre>
<div class="block">Stmt is the parent class of all Metamath <code>Hyp</code>s (hypotheses) and
 <code>Assrt</code>s.
 <p>
 Every Stmt has a label, which uniquely identifies it within the Stmt
 namespace (no rule against have a Stmt with a label equal to a Sym's id
 though.)
 <p>
 Every Stmt has a Formula, even <code>VarHyp</code>s.
 <p>
 Every Stmt also has a Type Code -- which is the first symbol of the Formula,
 and must be a Cnst. (This is a key point!) Everything following the Type Code
 in the Stmt's Formula is referred to in mmj as the "Expression" or the
 "Formula's Expression". (Make a note -- the nomenclature can be confusing,
 but Metamath requires every "formula" to have a Type Code, and what other
 books/works refer to as the "formula" equates to mmj's Expression.)
 <p>
 Metamath statements and their correspondence to mmj "Stmt":
 <ul>
 <li>$f -- mmj.lang.VarHyp.java (Variable Hypothesis, aka "floating")
 <li>$e -- mmj.lang.LogHyp.java (Logical Hypothesis)
 <li>$a -- mmj.lang.Axiom.java (aka "axiomatic assertion")
 <li>$p -- mmj.lang.Theorem.java (aka "provable assertion")
 <p>
 The only goofball Metamath statements that do not form mmj Stmt's, (other
 than Cnst ("$c") and Var ($v) which inherit from Sym), are:
 <ul>
 <li>$d -- mmj.lang.DjVars.java (Disjoint Variable Restriction)
 <li>$[ -- mmj.mmio.IncludeFile.java (terminating "$]")
 <li>$( -- Comment, not presently stored in mmj (terminating "$)")
 <li>${ -- mmj.lang.ScopeDef.java (terminating "$}")
 </ul></div>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../MetamathERNotes.html"> Nomenclature and
      Entity-Relationship Notes</a></dd></dl>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- =========== FIELD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="field_summary">
<!--   -->
</a>
<h3>Field Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Field Summary table, listing fields, and an explanation">
<caption><span>Fields</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Field and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static java.util.Comparator&lt;<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Stmt.html#DESC_NBR_PROOF_REFS">DESC_NBR_PROOF_REFS</a></strong></code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>protected <a href="../../mmj/lang/ParseTree.html" title="class in mmj.lang">ParseTree</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Stmt.html#exprParseTree">exprParseTree</a></strong></code>
<div class="block">exprRPN is the Reverse Polish Notation parse of the expression portion of
 a statement's formula (the 2nd through nth symbols).</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static java.util.Comparator&lt;<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Stmt.html#LABEL">LABEL</a></strong></code>
<div class="block">LABEL sequences by Stmt.label</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>protected java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Stmt.html#logHypsL1HiLoKey">logHypsL1HiLoKey</a></strong></code>
<div class="block">This contains the labels of the root node Syntax Axiom for the
 Assrt.logHypArray with lowest and greates sequence numbers.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>protected int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Stmt.html#logHypsMaxDepth">logHypsMaxDepth</a></strong></code>
<div class="block">This contains the greatest maximum depth among Parse Trees in the
 Assrt.logHypArray.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>protected int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Stmt.html#nbrProofRefs">nbrProofRefs</a></strong></code>&nbsp;</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="fields_inherited_from_class_mmj.lang.MObj">
<!--   -->
</a>
<h3>Fields inherited from class&nbsp;mmj.lang.<a href="../../mmj/lang/MObj.html" title="class in mmj.lang">MObj</a></h3>
<code><a href="../../mmj/lang/MObj.html#chapterNbr">chapterNbr</a>, <a href="../../mmj/lang/MObj.html#description">description</a>, <a href="../../mmj/lang/MObj.html#isTempObject">isTempObject</a>, <a href="../../mmj/lang/MObj.html#SECTION_AND_MOBJ_NBR">SECTION_AND_MOBJ_NBR</a>, <a href="../../mmj/lang/MObj.html#sectionMObjNbr">sectionMObjNbr</a>, <a href="../../mmj/lang/MObj.html#sectionNbr">sectionNbr</a>, <a href="../../mmj/lang/MObj.html#seq">seq</a>, <a href="../../mmj/lang/MObj.html#SEQ">SEQ</a></code></li>
</ul>
</li>
</ul>
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier</th>
<th class="colLast" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>&nbsp;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Stmt.html#Stmt(int, java.util.Map, java.util.Map, java.lang.String)">Stmt</a></strong>(int&nbsp;seq,
    java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTbl,
    java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;&nbsp;stmtTbl,
    java.lang.String&nbsp;labelS)</code>
<div class="block">Construct using sequence number and id string.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>protected </code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Stmt.html#Stmt(int, java.lang.String, mmj.lang.Formula, mmj.lang.ParseTree)">Stmt</a></strong>(int&nbsp;tempSeq,
    java.lang.String&nbsp;tempLabel,
    <a href="../../mmj/lang/Formula.html" title="class in mmj.lang">Formula</a>&nbsp;tempFormula,
    <a href="../../mmj/lang/ParseTree.html" title="class in mmj.lang">ParseTree</a>&nbsp;tempParseTree)</code>
<div class="block">Construct temp Stmt using precomputed values and doing no validation.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method_summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Method Summary table, listing methods, and an explanation">
<caption><span>Methods</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Method and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Stmt.html#equals(java.lang.Object)">equals</a></strong>(java.lang.Object&nbsp;obj)</code>
<div class="block">Compare for equality with another MObj.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/ParseTree.html" title="class in mmj.lang">ParseTree</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Stmt.html#getExprParseTree()">getExprParseTree</a></strong>()</code>
<div class="block">Get exprParseTree, the statement's parse tree.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/ParseTree.RPNStep.html" title="class in mmj.lang">ParseTree.RPNStep</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Stmt.html#getExprRPN()">getExprRPN</a></strong>()</code>
<div class="block">Return exprRPN, the statement's parse RPN.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/Formula.html" title="class in mmj.lang">Formula</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Stmt.html#getFormula()">getFormula</a></strong>()</code>
<div class="block">Return Stmt Formula.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Stmt.html#getLabel()">getLabel</a></strong>()</code>
<div class="block">Return Stmt label.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>abstract int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Stmt.html#getMandHypArrayLength()">getMandHypArrayLength</a></strong>()</code>
<div class="block">Return mandatory Hyp Array length Note: the Hyp array is different from
 the VarHyp array because the Hyp array can also include LogHyp's.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>abstract <a href="../../mmj/lang/VarHyp.html" title="class in mmj.lang">VarHyp</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Stmt.html#getMandVarHypArray()">getMandVarHypArray</a></strong>()</code>
<div class="block">Return mandatory VarHyp Array</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Stmt.html#getNbrProofRefs()">getNbrProofRefs</a></strong>()</code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Stmt.html#getTyp()">getTyp</a></strong>()</code>
<div class="block">Return Stmt Type Code.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Stmt.html#hashCode()">hashCode</a></strong>()</code>
<div class="block">Computes hashcode for this MObj</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Stmt.html#incrementNbrProofRefs()">incrementNbrProofRefs</a></strong>()</code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Stmt.html#initNbrProofRefs()">initNbrProofRefs</a></strong>()</code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>abstract boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Stmt.html#isActive()">isActive</a></strong>()</code>
<div class="block">Is Stmt active?</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>abstract int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Stmt.html#renderParsedSubExpr(java.lang.StringBuilder, int, int, mmj.lang.ParseNode[])">renderParsedSubExpr</a></strong>(java.lang.StringBuilder&nbsp;sb,
                   int&nbsp;maxDepth,
                   int&nbsp;maxLength,
                   <a href="../../mmj/lang/ParseNode.html" title="class in mmj.lang">ParseNode</a>[]&nbsp;child)</code>
<div class="block">Converts a parse sub-tree into a sub-expression which is output into a
 String Buffer.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Stmt.html#resetLogHypsL1HiLoKey()">resetLogHypsL1HiLoKey</a></strong>()</code>
<div class="block">Reset the computed Hi/Lo key for an Assertions LogHyps to the default
 value.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Stmt.html#resetLogHypsMaxDepth()">resetLogHypsMaxDepth</a></strong>()</code>
<div class="block">Reset the computed max depth value for the LogHyps in an Assrt to the
 default value.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Stmt.html#setExprParseTree(mmj.lang.ParseTree)">setExprParseTree</a></strong>(<a href="../../mmj/lang/ParseTree.html" title="class in mmj.lang">ParseTree</a>&nbsp;parseTree)</code>
<div class="block">Set exprParseTree, the statement's parse tree.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Stmt.html#setExprRPN(mmj.lang.ParseTree.RPNStep[])">setExprRPN</a></strong>(<a href="../../mmj/lang/ParseTree.RPNStep.html" title="class in mmj.lang">ParseTree.RPNStep</a>[]&nbsp;exprRPN)</code>
<div class="block">Set exprRPN, the statement's parse RPN.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Stmt.html#setLogHypsL1HiLoKey(java.lang.String)">setLogHypsL1HiLoKey</a></strong>(java.lang.String&nbsp;logHypsL1HiLoKey)</code>
<div class="block">Set the computed Hi/Lo key for an Assertions LogHyps.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Stmt.html#setLogHypsMaxDepth(int)">setLogHypsMaxDepth</a></strong>(int&nbsp;logHypsMaxDepth)</code>
<div class="block">Set the computed max depth value for the LogHyps in an Assrt.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Stmt.html#setTyp(mmj.lang.Cnst)">setTyp</a></strong>(<a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&nbsp;typ)</code>
<div class="block">Set Stmt Type Code.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Stmt.html#toString()">toString</a></strong>()</code>
<div class="block">Converts to String.</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_mmj.lang.MObj">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;mmj.lang.<a href="../../mmj/lang/MObj.html" title="class in mmj.lang">MObj</a></h3>
<code><a href="../../mmj/lang/MObj.html#getChapterNbr()">getChapterNbr</a>, <a href="../../mmj/lang/MObj.html#getDescription()">getDescription</a>, <a href="../../mmj/lang/MObj.html#getDescriptionForSearch()">getDescriptionForSearch</a>, <a href="../../mmj/lang/MObj.html#getIsTempObject()">getIsTempObject</a>, <a href="../../mmj/lang/MObj.html#getOrigSectionNbr()">getOrigSectionNbr</a>, <a href="../../mmj/lang/MObj.html#getSectionMObjNbr()">getSectionMObjNbr</a>, <a href="../../mmj/lang/MObj.html#getSectionNbr()">getSectionNbr</a>, <a href="../../mmj/lang/MObj.html#getSeq()">getSeq</a>, <a href="../../mmj/lang/MObj.html#setChapterNbr(int)">setChapterNbr</a>, <a href="../../mmj/lang/MObj.html#setDescription(java.lang.String)">setDescription</a>, <a href="../../mmj/lang/MObj.html#setIsTempObject(boolean)">setIsTempObject</a>, <a href="../../mmj/lang/MObj.html#setSectionMObjNbr(int)">setSectionMObjNbr</a>, <a href="../../mmj/lang/MObj.html#setSectionNbr(int)">setSectionNbr</a></code></li>
</ul>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.Object</h3>
<code>clone, finalize, getClass, notify, notifyAll, wait, wait, wait</code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ============ FIELD DETAIL =========== -->
<ul class="blockList">
<li class="blockList"><a name="field_detail">
<!--   -->
</a>
<h3>Field Detail</h3>
<a name="exprParseTree">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>exprParseTree</h4>
<pre>protected&nbsp;<a href="../../mmj/lang/ParseTree.html" title="class in mmj.lang">ParseTree</a> exprParseTree</pre>
<div class="block">exprRPN is the Reverse Polish Notation parse of the expression portion of
 a statement's formula (the 2nd through nth symbols). Every statement has
 a non-null exprRPN -- by definition. It is set by the SyntaxVerifier as
 follows:
 <ul>
 <li>VarHyp : label of the VarHyp Stmt itself.</li>
 <li>Syntax Axiom : labels of the Syntax Axiom's VarHyp's in database
 sequence followed by the label of the Syntax Axiom itself.</li>
 <li>other : RPN version of grammatical parse tree for the statement, if a
 unique valid grammatical parse is found; otherwise, defaults to VarHyp
 labels in database sequence followed by the label of the statement
 itself. If multiple parse trees exist, the first found is chosen (and a
 warning message is generated).
 </ul></div>
</li>
</ul>
<a name="logHypsMaxDepth">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>logHypsMaxDepth</h4>
<pre>protected&nbsp;int logHypsMaxDepth</pre>
<div class="block">This contains the greatest maximum depth among Parse Trees in the
 Assrt.logHypArray. It is stored here so that the value can be easily
 reinitialized by Grammar if the statements are reparsed and the parse
 trees are updated. The value is calculated dynamically, if and when
 needed in Assrt.</div>
</li>
</ul>
<a name="logHypsL1HiLoKey">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>logHypsL1HiLoKey</h4>
<pre>protected&nbsp;java.lang.String logHypsL1HiLoKey</pre>
<div class="block">This contains the labels of the root node Syntax Axiom for the
 Assrt.logHypArray with lowest and greates sequence numbers. If one of the
 LogHyp root nodes contains a VarHyp then the HiLoKey is set to the
 default value. We only want the computed value if every LogHyp has a
 Syntax Axiom in the root node of the parse tree. The Proof Assistant uses
 this field to reject candidate assertions from consideration for
 unification with a proof step. Because the Proof Assistant has to compute
 the order of LogHyps, we can rely only on the pair of Hi/Lo keys: if the
 candidate HiLo key is present and not equal to the proof step's LogHyps
 Hi/Lo key, then unification is impossible (i.e. this is a heuristic.) For
 example, if we know that there is a "wi" root node in the candidate
 assertion and the proof step's log hyps do not have a "wi" root node
 among them, then unification cannot be achieved. It is stored here so
 that the value can be easily reinitialized by Grammar if the statements
 are reparsed and the parse trees are updated. The value is calculated
 dynamically, if and when needed in Assrt.</div>
</li>
</ul>
<a name="nbrProofRefs">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>nbrProofRefs</h4>
<pre>protected&nbsp;int nbrProofRefs</pre>
</li>
</ul>
<a name="LABEL">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>LABEL</h4>
<pre>public static final&nbsp;java.util.Comparator&lt;<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt; LABEL</pre>
<div class="block">LABEL sequences by Stmt.label</div>
</li>
</ul>
<a name="DESC_NBR_PROOF_REFS">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>DESC_NBR_PROOF_REFS</h4>
<pre>public static final&nbsp;java.util.Comparator&lt;<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt; DESC_NBR_PROOF_REFS</pre>
</li>
</ul>
</li>
</ul>
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="Stmt(int, java.util.Map, java.util.Map, java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>Stmt</h4>
<pre>public&nbsp;Stmt(int&nbsp;seq,
    java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTbl,
    java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;&nbsp;stmtTbl,
    java.lang.String&nbsp;labelS)
     throws <a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></pre>
<div class="block">Construct using sequence number and id string.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>seq</code> - MObj.seq number</dd><dd><code>symTbl</code> - Symbol Table (Map)</dd><dd><code>stmtTbl</code> - Statement Table (Map)</dd><dd><code>labelS</code> - Stmt label string</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></code> - if label is empty string, or is a duplicate of
             another label in stmtTbl or an id in the symTbl.</dd></dl>
</li>
</ul>
<a name="Stmt(int, java.lang.String, mmj.lang.Formula, mmj.lang.ParseTree)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>Stmt</h4>
<pre>protected&nbsp;Stmt(int&nbsp;tempSeq,
    java.lang.String&nbsp;tempLabel,
    <a href="../../mmj/lang/Formula.html" title="class in mmj.lang">Formula</a>&nbsp;tempFormula,
    <a href="../../mmj/lang/ParseTree.html" title="class in mmj.lang">ParseTree</a>&nbsp;tempParseTree)</pre>
<div class="block">Construct temp Stmt using precomputed values and doing no validation.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>tempSeq</code> - MObj.seq</dd><dd><code>tempLabel</code> - Stmt.label</dd><dd><code>tempFormula</code> - Stmt.formula</dd><dd><code>tempParseTree</code> - Stmt.exprParseTree</dd></dl>
</li>
</ul>
</li>
</ul>
<!-- ============ METHOD DETAIL ========== -->
<ul class="blockList">
<li class="blockList"><a name="method_detail">
<!--   -->
</a>
<h3>Method Detail</h3>
<a name="isActive()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>isActive</h4>
<pre>public abstract&nbsp;boolean&nbsp;isActive()</pre>
<div class="block">Is Stmt active?
 <p>
 A Stmt defined at the global level -- outside of any scope -- is always
 active.
 <p>
 A statement defined inside a non-global scope level can only be referred
 to within that scope level or another scope level nested within the
 first.
 <p>
 Note: <code>Stmt</code>s refer to other <code>Stmt</code>s only within proofs and
 exprRPN (grammatical parses), but since Syntax Axioms must be defined at
 the global level, the question of a Stmt being "active" is only relevant
 to proofs.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>is Stmt "active"</dd></dl>
</li>
</ul>
<a name="getMandVarHypArray()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getMandVarHypArray</h4>
<pre>public abstract&nbsp;<a href="../../mmj/lang/VarHyp.html" title="class in mmj.lang">VarHyp</a>[]&nbsp;getMandVarHypArray()</pre>
<div class="block">Return mandatory VarHyp Array</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>mandatory VarHyp Array</dd></dl>
</li>
</ul>
<a name="getMandHypArrayLength()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getMandHypArrayLength</h4>
<pre>public abstract&nbsp;int&nbsp;getMandHypArrayLength()</pre>
<div class="block">Return mandatory Hyp Array length Note: the Hyp array is different from
 the VarHyp array because the Hyp array can also include LogHyp's.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>mandatory Hyp Array Length</dd></dl>
</li>
</ul>
<a name="renderParsedSubExpr(java.lang.StringBuilder, int, int, mmj.lang.ParseNode[])">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>renderParsedSubExpr</h4>
<pre>public abstract&nbsp;int&nbsp;renderParsedSubExpr(java.lang.StringBuilder&nbsp;sb,
                      int&nbsp;maxDepth,
                      int&nbsp;maxLength,
                      <a href="../../mmj/lang/ParseNode.html" title="class in mmj.lang">ParseNode</a>[]&nbsp;child)</pre>
<div class="block">Converts a parse sub-tree into a sub-expression which is output into a
 String Buffer.
 <p>
 Note: this will not work for a proof node! The ParseNode's stmt must be a
 VarHyp or a Syntax Axiom.
 <p>
 The output sub-expression is generated into text not to exceed the given
 maxLength. If the number of output characters exceeds maxLength output
 terminates, possibly leaving a dirty StringBuilder.
 <p>
 The depth of the sub-tree is checked against the input maxDepth
 parameter, and if the depth exceeds this number, output terminates,,
 possibly leaving a dirty StringBuilder.
 <p>
 Depth is computed as 1 for each Notation Syntax Axiom Node. VarHyp nodes
 and Nulls Permitted, Type Conversion and NamedTypedConstant Syntax Axiom
 nodes are assigned depth = 0 for purposes of depth checking.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>sb</code> - StringBuilder already initialized for appending characters.</dd><dd><code>maxDepth</code> - maximum depth of Notation Syntax axioms in sub-tree to be
            printed. Set to Integer.MAX_VALUE to turn off depth checking.</dd><dd><code>maxLength</code> - maximum length of output sub-expression. Set to
            Integer.MAX_VALUE to turn off depth checking.</dd><dd><code>child</code> - array of ParseNode, corresponding to VarHyp nodes to be
            substituted into the Stmt.</dd>
<dt><span class="strong">Returns:</span></dt><dd>length of sub-expression characters appended to the input
         StringBuilder -- or -1 if maxDepth or maxLength exceeded.</dd></dl>
</li>
</ul>
<a name="getLabel()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getLabel</h4>
<pre>public&nbsp;java.lang.String&nbsp;getLabel()</pre>
<div class="block">Return Stmt label.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>Stmt label</dd></dl>
</li>
</ul>
<a name="getFormula()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getFormula</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Formula.html" title="class in mmj.lang">Formula</a>&nbsp;getFormula()</pre>
<div class="block">Return Stmt Formula.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>Stmt Formula</dd></dl>
</li>
</ul>
<a name="getTyp()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getTyp</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&nbsp;getTyp()</pre>
<div class="block">Return Stmt Type Code.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>Stmt Type Code.</dd></dl>
</li>
</ul>
<a name="setTyp(mmj.lang.Cnst)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>setTyp</h4>
<pre>public&nbsp;void&nbsp;setTyp(<a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&nbsp;typ)</pre>
<div class="block">Set Stmt Type Code.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>typ</code> - Stmt Type Code.</dd></dl>
</li>
</ul>
<a name="getExprRPN()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getExprRPN</h4>
<pre>public&nbsp;<a href="../../mmj/lang/ParseTree.RPNStep.html" title="class in mmj.lang">ParseTree.RPNStep</a>[]&nbsp;getExprRPN()</pre>
<div class="block">Return exprRPN, the statement's parse RPN.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>exprRPN.</dd></dl>
</li>
</ul>
<a name="setExprRPN(mmj.lang.ParseTree.RPNStep[])">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>setExprRPN</h4>
<pre>public&nbsp;void&nbsp;setExprRPN(<a href="../../mmj/lang/ParseTree.RPNStep.html" title="class in mmj.lang">ParseTree.RPNStep</a>[]&nbsp;exprRPN)</pre>
<div class="block">Set exprRPN, the statement's parse RPN.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>exprRPN</code> - array of Stmt!</dd></dl>
</li>
</ul>
<a name="setLogHypsMaxDepth(int)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>setLogHypsMaxDepth</h4>
<pre>public&nbsp;void&nbsp;setLogHypsMaxDepth(int&nbsp;logHypsMaxDepth)</pre>
<div class="block">Set the computed max depth value for the LogHyps in an Assrt. The
 set/reset functions are here for convenience of updating via Grammar when
 statements are reparsed.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>logHypsMaxDepth</code> - the new max depth value</dd></dl>
</li>
</ul>
<a name="resetLogHypsMaxDepth()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>resetLogHypsMaxDepth</h4>
<pre>public&nbsp;void&nbsp;resetLogHypsMaxDepth()</pre>
<div class="block">Reset the computed max depth value for the LogHyps in an Assrt to the
 default value.</div>
</li>
</ul>
<a name="setLogHypsL1HiLoKey(java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>setLogHypsL1HiLoKey</h4>
<pre>public&nbsp;void&nbsp;setLogHypsL1HiLoKey(java.lang.String&nbsp;logHypsL1HiLoKey)</pre>
<div class="block">Set the computed Hi/Lo key for an Assertions LogHyps. The set/reset
 functions are here for convenience of updating via Grammar when
 statements are reparsed.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>logHypsL1HiLoKey</code> - computed value.</dd></dl>
</li>
</ul>
<a name="resetLogHypsL1HiLoKey()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>resetLogHypsL1HiLoKey</h4>
<pre>public&nbsp;void&nbsp;resetLogHypsL1HiLoKey()</pre>
<div class="block">Reset the computed Hi/Lo key for an Assertions LogHyps to the default
 value.</div>
</li>
</ul>
<a name="getExprParseTree()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getExprParseTree</h4>
<pre>public&nbsp;<a href="../../mmj/lang/ParseTree.html" title="class in mmj.lang">ParseTree</a>&nbsp;getExprParseTree()</pre>
<div class="block">Get exprParseTree, the statement's parse tree.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>exprParseTree Parse Tree from Grammar</dd></dl>
</li>
</ul>
<a name="setExprParseTree(mmj.lang.ParseTree)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>setExprParseTree</h4>
<pre>public&nbsp;void&nbsp;setExprParseTree(<a href="../../mmj/lang/ParseTree.html" title="class in mmj.lang">ParseTree</a>&nbsp;parseTree)</pre>
<div class="block">Set exprParseTree, the statement's parse tree.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>parseTree</code> - Parse Tree from Grammar</dd></dl>
</li>
</ul>
<a name="getNbrProofRefs()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getNbrProofRefs</h4>
<pre>public&nbsp;int&nbsp;getNbrProofRefs()</pre>
</li>
</ul>
<a name="initNbrProofRefs()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>initNbrProofRefs</h4>
<pre>public&nbsp;void&nbsp;initNbrProofRefs()</pre>
</li>
</ul>
<a name="incrementNbrProofRefs()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>incrementNbrProofRefs</h4>
<pre>public&nbsp;int&nbsp;incrementNbrProofRefs()</pre>
</li>
</ul>
<a name="toString()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>toString</h4>
<pre>public&nbsp;java.lang.String&nbsp;toString()</pre>
<div class="block">Converts to String.
 <p>
 Output is simply Stmt.label.</div>
<dl>
<dt><strong>Overrides:</strong></dt>
<dd><code><a href="../../mmj/lang/MObj.html#toString()">toString</a></code>&nbsp;in class&nbsp;<code><a href="../../mmj/lang/MObj.html" title="class in mmj.lang">MObj</a></code></dd>
<dt><span class="strong">Returns:</span></dt><dd>returns Stmt string;</dd></dl>
</li>
</ul>
<a name="hashCode()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>hashCode</h4>
<pre>public&nbsp;int&nbsp;hashCode()</pre>
<div class="block"><strong>Description copied from class:&nbsp;<code><a href="../../mmj/lang/MObj.html#hashCode()">MObj</a></code></strong></div>
<div class="block">Computes hashcode for this MObj</div>
<dl>
<dt><strong>Overrides:</strong></dt>
<dd><code><a href="../../mmj/lang/MObj.html#hashCode()">hashCode</a></code>&nbsp;in class&nbsp;<code><a href="../../mmj/lang/MObj.html" title="class in mmj.lang">MObj</a></code></dd>
<dt><span class="strong">Returns:</span></dt><dd>hashcode for the MObj</dd></dl>
</li>
</ul>
<a name="equals(java.lang.Object)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>equals</h4>
<pre>public&nbsp;boolean&nbsp;equals(java.lang.Object&nbsp;obj)</pre>
<div class="block"><strong>Description copied from class:&nbsp;<code><a href="../../mmj/lang/MObj.html#equals(java.lang.Object)">MObj</a></code></strong></div>
<div class="block">Compare for equality with another MObj.
 <p>
 Equal if and only if the MObj sequence numbers are equal. and the obj to
 be compared to this object is not null and is a MObj as well.</div>
<dl>
<dt><strong>Overrides:</strong></dt>
<dd><code><a href="../../mmj/lang/MObj.html#equals(java.lang.Object)">equals</a></code>&nbsp;in class&nbsp;<code><a href="../../mmj/lang/MObj.html" title="class in mmj.lang">MObj</a></code></dd>
<dt><span class="strong">Returns:</span></dt><dd>returns true if equal, otherwise false.</dd></dl>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar_bottom">
<!--   -->
</a><a href="#skip-navbar_bottom" title="Skip navigation links"></a><a name="navbar_bottom_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/lang/SeqAssigner.html" title="class in mmj.lang"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/lang/Sym.html" title="class in mmj.lang"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/lang/Stmt.html" target="_top">Frames</a></li>
<li><a href="Stmt.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li><a href="#field_summary">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li><a href="#field_detail">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
